PittsburghV1, Main, Exploration, bibRecord, 000097

A Method for Invariant Generation for Polynomial Continuous Systems

Identifieur interne : 000097 ( Main/Exploration ); précédent : 000096; suivant : 000098

A Method for Invariant Generation for Polynomial Continuous Systems

Auteurs : Andrew Sogokon [Royaume-Uni] ; Khalil Ghorbal [France] ; Paul Jackson [Royaume-Uni] ; André Platzer [États-Unis]

Source :

RBID : Hal:hal-01374902

Abstract

This paper presents a method for generating semi-algebraic invariants for systems governed by non-linear polynomial ordinary differential equations under semi-algebraic evolution constraints. Based on the notion of discrete abstraction , our method eliminates unsoundness and unnecessary coarseness found in existing approaches for computing abstractions for non-linear continuous systems and is able to construct invariants with intricate boolean structure, in contrast to invariants typically generated using template-based methods. In order to tackle the state explosion problem associated with discrete abstraction, we present invariant generation algorithms that exploit sound proof rules for safety verification , such as differential cut (DC), and a new proof rule that we call differential divide-and-conquer (DDC), which splits the verification problem into smaller sub-problems. The resulting invariant generation method is observed to be much more scalable and efficient than the na¨ıvena¨ıve approach, exhibiting orders of magnitude performance improvement on many of the problems.

Url:

https://hal.archives-ouvertes.fr/hal-01374902

DOI: 10.1007/978-3-662-49122-5_13

Affiliations:

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: 000024
to stream Hal, to step Curation: 000024
to stream Hal, to step Checkpoint: 000096
to stream Main, to step Merge: 000097
to stream Main, to step Curation: 000097

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Method for Invariant Generation for Polynomial Continuous Systems</title>
<author><name sortKey="Sogokon, Andrew" sort="Sogokon, Andrew" uniqKey="Sogokon A" first="Andrew" last="Sogokon">Andrew Sogokon</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-182763" status="VALID"><orgName>School of Informatics [Edimbourg]</orgName>
<desc><address><addrLine>Informatics Forum 10 Crichton Street Edinburgh EH8 9AB</addrLine>
<country key="GB"></country>
</address>
<ref type="url">http://www.ed.ac.uk/schools-departments/informatics/</ref>
</desc>
<listRelation><relation active="#struct-61277" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-61277" type="direct"><org type="institution" xml:id="struct-61277" status="VALID">          <orgName>University of Edinburgh</orgName>
          <desc>            <address>              <addrLine>Old College South Bridge Edinburgh EH8 9YL</addrLine>
              <country key="GB"></country>
            </address>
            <ref type="url">http://www.ed.ac.uk/home</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Royaume-Uni</country>
<placeName><settlement type="city">Édimbourg</settlement>
<region type="country">Écosse</region>
</placeName>
<orgName type="university">Université d'Édimbourg</orgName>
</affiliation>
</author>
<author><name sortKey="Ghorbal, Khalil" sort="Ghorbal, Khalil" uniqKey="Ghorbal K" first="Khalil" last="Ghorbal">Khalil Ghorbal</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-419153" status="VALID"><idno type="RNSR">198018249C</idno>
<orgName>Inria Rennes – Bretagne Atlantique </orgName>
<desc><address><addrLine>Campus de beaulieu35042 Rennes cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre/rennes</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Jackson, Paul" sort="Jackson, Paul" uniqKey="Jackson P" first="Paul" last="Jackson">Paul Jackson</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-182763" status="VALID"><orgName>School of Informatics [Edimbourg]</orgName>
<desc><address><addrLine>Informatics Forum 10 Crichton Street Edinburgh EH8 9AB</addrLine>
<country key="GB"></country>
</address>
<ref type="url">http://www.ed.ac.uk/schools-departments/informatics/</ref>
</desc>
<listRelation><relation active="#struct-61277" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-61277" type="direct"><org type="institution" xml:id="struct-61277" status="VALID">          <orgName>University of Edinburgh</orgName>
          <desc>            <address>              <addrLine>Old College South Bridge Edinburgh EH8 9YL</addrLine>
              <country key="GB"></country>
            </address>
            <ref type="url">http://www.ed.ac.uk/home</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Royaume-Uni</country>
<placeName><settlement type="city">Édimbourg</settlement>
<region type="country">Écosse</region>
</placeName>
<orgName type="university">Université d'Édimbourg</orgName>
</affiliation>
</author>
<author><name sortKey="Platzer, Andre" sort="Platzer, Andre" uniqKey="Platzer A" first="André" last="Platzer">André Platzer</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-67135" status="VALID">          <orgName>Carnegie Mellon University [Pittsburgh]</orgName>
          <orgName type="acronym">CMU</orgName>
          <desc>            <address>              <addrLine>5000 Forbes Ave,  Pittsburgh, PA 15213</addrLine>
              <country key="US"></country>
            </address>
            <ref type="url">http://www.cmu.edu/</ref>
          </desc>
        </hal:affiliation>
<country>États-Unis</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01374902</idno>
<idno type="halId">hal-01374902</idno>
<idno type="halUri">https://hal.archives-ouvertes.fr/hal-01374902</idno>
<idno type="url">https://hal.archives-ouvertes.fr/hal-01374902</idno>
<idno type="doi">10.1007/978-3-662-49122-5_13</idno>
<date when="2016-01-17">2016-01-17</date>
<idno type="wicri:Area/Hal/Corpus">000024</idno>
<idno type="wicri:Area/Hal/Curation">000024</idno>
<idno type="wicri:Area/Hal/Checkpoint">000096</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000096</idno>
<idno type="wicri:Area/Main/Merge">000097</idno>
<idno type="wicri:Area/Main/Curation">000097</idno>
<idno type="wicri:Area/Main/Exploration">000097</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">A Method for Invariant Generation for Polynomial Continuous Systems</title>
<author><name sortKey="Sogokon, Andrew" sort="Sogokon, Andrew" uniqKey="Sogokon A" first="Andrew" last="Sogokon">Andrew Sogokon</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-182763" status="VALID"><orgName>School of Informatics [Edimbourg]</orgName>
<desc><address><addrLine>Informatics Forum 10 Crichton Street Edinburgh EH8 9AB</addrLine>
<country key="GB"></country>
</address>
<ref type="url">http://www.ed.ac.uk/schools-departments/informatics/</ref>
</desc>
<listRelation><relation active="#struct-61277" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-61277" type="direct"><org type="institution" xml:id="struct-61277" status="VALID">          <orgName>University of Edinburgh</orgName>
          <desc>            <address>              <addrLine>Old College South Bridge Edinburgh EH8 9YL</addrLine>
              <country key="GB"></country>
            </address>
            <ref type="url">http://www.ed.ac.uk/home</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Royaume-Uni</country>
<placeName><settlement type="city">Édimbourg</settlement>
<region type="country">Écosse</region>
</placeName>
<orgName type="university">Université d'Édimbourg</orgName>
</affiliation>
</author>
<author><name sortKey="Ghorbal, Khalil" sort="Ghorbal, Khalil" uniqKey="Ghorbal K" first="Khalil" last="Ghorbal">Khalil Ghorbal</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-419153" status="VALID"><idno type="RNSR">198018249C</idno>
<orgName>Inria Rennes – Bretagne Atlantique </orgName>
<desc><address><addrLine>Campus de beaulieu35042 Rennes cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre/rennes</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Jackson, Paul" sort="Jackson, Paul" uniqKey="Jackson P" first="Paul" last="Jackson">Paul Jackson</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-182763" status="VALID"><orgName>School of Informatics [Edimbourg]</orgName>
<desc><address><addrLine>Informatics Forum 10 Crichton Street Edinburgh EH8 9AB</addrLine>
<country key="GB"></country>
</address>
<ref type="url">http://www.ed.ac.uk/schools-departments/informatics/</ref>
</desc>
<listRelation><relation active="#struct-61277" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-61277" type="direct"><org type="institution" xml:id="struct-61277" status="VALID">          <orgName>University of Edinburgh</orgName>
          <desc>            <address>              <addrLine>Old College South Bridge Edinburgh EH8 9YL</addrLine>
              <country key="GB"></country>
            </address>
            <ref type="url">http://www.ed.ac.uk/home</ref>
          </desc>
        </org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Royaume-Uni</country>
<placeName><settlement type="city">Édimbourg</settlement>
<region type="country">Écosse</region>
</placeName>
<orgName type="university">Université d'Édimbourg</orgName>
</affiliation>
</author>
<author><name sortKey="Platzer, Andre" sort="Platzer, Andre" uniqKey="Platzer A" first="André" last="Platzer">André Platzer</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-67135" status="VALID">          <orgName>Carnegie Mellon University [Pittsburgh]</orgName>
          <orgName type="acronym">CMU</orgName>
          <desc>            <address>              <addrLine>5000 Forbes Ave,  Pittsburgh, PA 15213</addrLine>
              <country key="US"></country>
            </address>
            <ref type="url">http://www.cmu.edu/</ref>
          </desc>
        </hal:affiliation>
<country>États-Unis</country>
</affiliation>
</author>
</analytic>
<idno type="DOI">10.1007/978-3-662-49122-5_13</idno>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">This paper presents a method for generating semi-algebraic invariants for systems governed by non-linear polynomial ordinary differential equations under semi-algebraic evolution constraints. Based on the notion of discrete abstraction , our method eliminates unsoundness and unnecessary coarseness found in existing approaches for computing abstractions for non-linear continuous systems and is able to construct invariants with intricate boolean structure, in contrast to invariants typically generated using template-based methods. In order to tackle the state explosion problem associated with discrete abstraction, we present invariant generation algorithms that exploit sound proof rules for safety verification , such as differential cut (DC), and a new proof rule that we call differential divide-and-conquer (DDC), which splits the verification problem into smaller sub-problems. The resulting invariant generation method is observed to be much more scalable and efficient than the na¨ıvena¨ıve approach, exhibiting orders of magnitude performance improvement on many of the problems.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Royaume-Uni</li>
<li>États-Unis</li>
</country>
<region><li>Écosse</li>
</region>
<settlement><li>Édimbourg</li>
</settlement>
<orgName><li>Université d'Édimbourg</li>
</orgName>
</list>
<tree><country name="Royaume-Uni"><region name="Écosse"><name sortKey="Sogokon, Andrew" sort="Sogokon, Andrew" uniqKey="Sogokon A" first="Andrew" last="Sogokon">Andrew Sogokon</name>
</region>
<name sortKey="Jackson, Paul" sort="Jackson, Paul" uniqKey="Jackson P" first="Paul" last="Jackson">Paul Jackson</name>
</country>
<country name="France"><noRegion><name sortKey="Ghorbal, Khalil" sort="Ghorbal, Khalil" uniqKey="Ghorbal K" first="Khalil" last="Ghorbal">Khalil Ghorbal</name>
</noRegion>
</country>
<country name="États-Unis"><noRegion><name sortKey="Platzer, Andre" sort="Platzer, Andre" uniqKey="Platzer A" first="André" last="Platzer">André Platzer</name>
</noRegion>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Amérique/explor/PittsburghV1/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000097 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000097 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Amérique
   |area=    PittsburghV1
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Hal:hal-01374902
   |texte=   A Method for Invariant Generation for Polynomial Continuous Systems
}}

This area was generated with Dilib version V0.6.38.
Data generation: Fri Jun 18 17:37:45 2021. Site generation: Fri Jun 18 18:15:47 2021

	Serveur d'exploration sur Pittsburgh
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur Pittsburgh

A Method for Invariant Generation for Polynomial Continuous Systems

A Method for Invariant Generation for Polynomial Continuous Systems

Source :

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri